The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

f1 → g1
f1 → g2
f2 → g1
f2 → g2
g1 → h1
g1 → h2
g2 → h1
g2 → h2
h1 → i
h2 → i
e1(h1, h2, x, y, z) → e2(x, x, y, z, z)
e1(x1, x1, x, y, z) → e5(x1, x, y, z)
e2(f1, x, y, z, f2) → e3(x, y, x, y, y, z, y, z, x, y, z)
e2(x, x, y, z, z) → e6(x, y, z)
e2(i, x, y, z, i) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3(x, y, x, y, y, z, y, z, x, y, z) → e6(x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) → e1(x1, x1, x, y, z)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
e1(h1, h2, x, y, z) → e2(x, x, y, z, z)
e2(f1, x, y, z, f2) → e3(x, y, x, y, y, z, y, z, x, y, z)
e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) → e1(x1, x1, x, y, z)

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

h1 → i
f2 → g2
f1 → g1
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) → e5(x1, x, y, z)
f1 → g2
f2 → g1
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3(x, y, x, y, y, z, y, z, x, y, z) → e6(x, y, z)
e2(i, x, y, z, i) → e6(x, y, z)
e5(i, x, y, z) → e6(x, y, z)
g2 → h1
g1 → h1
g2 → h2
e1(x1, x1, x, y, z) → e5(x1, x, y, z)
e2(x, x, y, z, z) → e6(x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x) → e6(x, x, x)
g1 → h2
h2 → i

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

h1 → i [1]
f2 → g2 [1]
f1 → g1 [1]
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) → e5(x1, x, y, z) [1]
f1 → g2 [1]
f2 → g1 [1]
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) [1]
e3(x, y, x, y, y, z, y, z, x, y, z) → e6(x, y, z) [1]
e2(i, x, y, z, i) → e6(x, y, z) [1]
e5(i, x, y, z) → e6(x, y, z) [1]
g2 → h1 [1]
g1 → h1 [1]
g2 → h2 [1]
e1(x1, x1, x, y, z) → e5(x1, x, y, z) [1]
e2(x, x, y, z, z) → e6(x, y, z) [1]
e4(x, x, x, x, x, x, x, x, x, x, x) → e6(x, x, x) [1]
g1 → h2 [1]
h2 → i [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

h1 → i [1]
f2 → g2 [1]
f1 → g1 [1]
e4(i, x1, i, x1, i, x1, i, x1, x, y, z) → e5(x1, x, y, z) [1]
f1 → g2 [1]
f2 → g1 [1]
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) [1]
e3(x, y, x, y, y, z, y, z, x, y, z) → e6(x, y, z) [1]
e2(i, x, y, z, i) → e6(x, y, z) [1]
e5(i, x, y, z) → e6(x, y, z) [1]
g2 → h1 [1]
g1 → h1 [1]
g2 → h2 [1]
e1(x1, x1, x, y, z) → e5(x1, x, y, z) [1]
e2(x, x, y, z, z) → e6(x, y, z) [1]
e4(x, x, x, x, x, x, x, x, x, x, x) → e6(x, x, x) [1]
g1 → h2 [1]
h2 → i [1]

The TRS has the following type information:

h1 :: i i :: i f2 :: i g2 :: i f1 :: i g1 :: i e4 :: i → i → i → i → i → i → i → i → i → i → i → e6 e5 :: i → i → i → i → e6 e3 :: i → i → i → i → i → i → i → i → i → i → i → e6 e6 :: i → i → i → e6 e2 :: i → i → i → i → i → e6 h2 :: i e1 :: i → i → i → i → i → e6

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

e4(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10) → null_e4 [0]
e3(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10) → null_e3 [0]
e1(v0, v1, v2, v3, v4) → null_e1 [0]

And the following fresh constants:

null_e4, null_e3, null_e1

(8) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: h1 → i [1] f2 → g2 [1] f1 → g1 [1] e4(i, x1, i, x1, i, x1, i, x1, x, y, z) → e5(x1, x, y, z) [1] f1 → g2 [1] f2 → g1 [1] e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) [1] e3(x, y, x, y, y, z, y, z, x, y, z) → e6(x, y, z) [1] e2(i, x, y, z, i) → e6(x, y, z) [1] e5(i, x, y, z) → e6(x, y, z) [1] g2 → h1 [1] g1 → h1 [1] g2 → h2 [1] e1(x1, x1, x, y, z) → e5(x1, x, y, z) [1] e2(x, x, y, z, z) → e6(x, y, z) [1] e4(x, x, x, x, x, x, x, x, x, x, x) → e6(x, x, x) [1] g1 → h2 [1] h2 → i [1] e4(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10) → null_e4 [0] e3(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10) → null_e3 [0] e1(v0, v1, v2, v3, v4) → null_e1 [0] The TRS has the following type information: h1 :: i i :: i f2 :: i g2 :: i f1 :: i g1 :: i e4 :: i → i → i → i → i → i → i → i → i → i → i → e6:null_e4:null_e3:null_e1 e5 :: i → i → i → i → e6:null_e4:null_e3:null_e1 e3 :: i → i → i → i → i → i → i → i → i → i → i → e6:null_e4:null_e3:null_e1 e6 :: i → i → i → e6:null_e4:null_e3:null_e1 e2 :: i → i → i → i → i → e6:null_e4:null_e3:null_e1 h2 :: i e1 :: i → i → i → i → i → e6:null_e4:null_e3:null_e1 null_e4 :: e6:null_e4:null_e3:null_e1 null_e3 :: e6:null_e4:null_e3:null_e1 null_e1 :: e6:null_e4:null_e3:null_e1 Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

i => 0
null_e4 => 0
null_e3 => 0
null_e1 => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

e1(z', z'', z1, z2, z3) -{ 1 }→ e5(x1, x, y, z) :|: z'' = x1, z2 = y, x1 >= 0, z >= 0, z3 = z, x >= 0, y >= 0, z' = x1, z1 = x
e1(z', z'', z1, z2, z3) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, v4 >= 0, z1 = v2, v1 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0
e2(z', z'', z1, z2, z3) -{ 1 }→ 1 + x + y + z :|: z1 = y, z >= 0, z2 = z, z3 = 0, x >= 0, y >= 0, z'' = x, z' = 0
e2(z', z'', z1, z2, z3) -{ 1 }→ 1 + x + y + z :|: z1 = y, z >= 0, z' = x, z2 = z, z3 = z, x >= 0, y >= 0, z'' = x
e3(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9) -{ 1 }→ e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) :|: z5 = x4, z7 = x, z1 = x2, y >= 0, z' = x1, z2 = x2, z3 = x3, z4 = x3, x2 >= 0, x3 >= 0, z'' = x1, z9 = z, x1 >= 0, x4 >= 0, z >= 0, x >= 0, z6 = x4, z8 = y
e3(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9) -{ 0 }→ 0 :|: z4 = v5, v0 >= 0, v8 >= 0, z8 = v9, z9 = v10, v6 >= 0, v1 >= 0, v5 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0, z2 = v3, v4 >= 0, z5 = v6, z1 = v2, v7 >= 0, v9 >= 0, v10 >= 0, z6 = v7, z7 = v8
e3(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9) -{ 1 }→ 1 + x + y + z :|: z7 = x, z' = x, z'' = y, z3 = y, y >= 0, z1 = x, z2 = y, z4 = z, z5 = y, z9 = z, z >= 0, x >= 0, z6 = z, z8 = y
e4(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9) -{ 1 }→ e5(x1, x, y, z) :|: z5 = 0, z7 = x, z2 = x1, z3 = 0, y >= 0, z6 = x1, z' = 0, z'' = x1, z1 = 0, z4 = x1, z9 = z, x1 >= 0, z >= 0, x >= 0, z8 = y
e4(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9) -{ 0 }→ 0 :|: z4 = v5, v0 >= 0, v8 >= 0, z8 = v9, z9 = v10, v6 >= 0, v1 >= 0, v5 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0, z2 = v3, v4 >= 0, z5 = v6, z1 = v2, v7 >= 0, v9 >= 0, v10 >= 0, z6 = v7, z7 = v8
e4(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9) -{ 1 }→ 1 + x + x + x :|: z2 = x, z3 = x, z6 = x, z7 = x, z' = x, z4 = x, z5 = x, x >= 0, z'' = x, z1 = x, z8 = x, z9 = x
e5(z', z'', z1, z2) -{ 1 }→ 1 + x + y + z :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0
f1 -{ 1 }→ g2 :|:
f1 -{ 1 }→ g1 :|:
f2 -{ 1 }→ g2 :|:
f2 -{ 1 }→ g1 :|:
g1 -{ 1 }→ h2 :|:
g1 -{ 1 }→ h1 :|:
g2 -{ 1 }→ h2 :|:
g2 -{ 1 }→ h1 :|:
h1 -{ 1 }→ 0 :|:
h2 -{ 1 }→ 0 :|:

Only complete derivations are relevant for the runtime complexity.

(11) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[h1(Out)],[]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[f2(Out)],[]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[f1(Out)],[]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[e4(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0,V5 >= 0,V6 >= 0,V7 >= 0,V8 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[e3(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0,V5 >= 0,V6 >= 0,V7 >= 0,V8 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[e2(V, V1, V2, V3, V4, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[e5(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[g2(Out)],[]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[g1(Out)],[]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[e1(V, V1, V2, V3, V4, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10),0,[h2(Out)],[]). eq(h1(Out),1,[],[Out = 0]). eq(f2(Out),1,[g2(Ret)],[Out = Ret]). eq(f1(Out),1,[g1(Ret1)],[Out = Ret1]). eq(e4(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out),1,[e5(V11, V12, V13, V14, Ret2)],[Out = Ret2,V6 = 0,V8 = V12,V3 = V11,V4 = 0,V13 >= 0,V7 = V11,V = 0,V1 = V11,V2 = 0,V5 = V11,V10 = V14,V11 >= 0,V14 >= 0,V12 >= 0,V9 = V13]). eq(f1(Out),1,[g2(Ret3)],[Out = Ret3]). eq(f2(Out),1,[g1(Ret4)],[Out = Ret4]). eq(e3(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out),1,[e4(V15, V15, V16, V16, V17, V17, V18, V18, V19, V20, V21, Ret5)],[Out = Ret5,V6 = V18,V8 = V19,V2 = V16,V20 >= 0,V = V15,V3 = V16,V4 = V17,V5 = V17,V16 >= 0,V17 >= 0,V1 = V15,V10 = V21,V15 >= 0,V18 >= 0,V21 >= 0,V19 >= 0,V7 = V18,V9 = V20]). eq(e3(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out),1,[],[Out = 1 + V22 + V23 + V24,V8 = V22,V = V22,V1 = V23,V4 = V23,V23 >= 0,V2 = V22,V3 = V23,V5 = V24,V6 = V23,V10 = V24,V24 >= 0,V22 >= 0,V7 = V24,V9 = V23]). eq(e2(V, V1, V2, V3, V4, Out),1,[],[Out = 1 + V25 + V26 + V27,V2 = V26,V27 >= 0,V3 = V27,V4 = 0,V25 >= 0,V26 >= 0,V1 = V25,V = 0]). eq(e5(V, V1, V2, V3, Out),1,[],[Out = 1 + V28 + V29 + V30,V2 = V29,V30 >= 0,V3 = V30,V28 >= 0,V29 >= 0,V1 = V28,V = 0]). eq(g2(Out),1,[h1(Ret6)],[Out = Ret6]). eq(g1(Out),1,[h1(Ret7)],[Out = Ret7]). eq(g2(Out),1,[h2(Ret8)],[Out = Ret8]). eq(e1(V, V1, V2, V3, V4, Out),1,[e5(V31, V32, V33, V34, Ret9)],[Out = Ret9,V1 = V31,V3 = V33,V31 >= 0,V34 >= 0,V4 = V34,V32 >= 0,V33 >= 0,V = V31,V2 = V32]). eq(e2(V, V1, V2, V3, V4, Out),1,[],[Out = 1 + V35 + V36 + V37,V2 = V36,V37 >= 0,V = V35,V3 = V37,V4 = V37,V35 >= 0,V36 >= 0,V1 = V35]). eq(e4(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out),1,[],[Out = 1 + 3*V38,V3 = V38,V4 = V38,V7 = V38,V8 = V38,V = V38,V5 = V38,V6 = V38,V38 >= 0,V1 = V38,V2 = V38,V9 = V38,V10 = V38]). eq(g1(Out),1,[h2(Ret10)],[Out = Ret10]). eq(h2(Out),1,[],[Out = 0]). eq(e4(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out),0,[],[Out = 0,V5 = V39,V40 >= 0,V41 >= 0,V9 = V42,V10 = V43,V44 >= 0,V45 >= 0,V39 >= 0,V1 = V45,V4 = V46,V47 >= 0,V48 >= 0,V = V40,V3 = V48,V46 >= 0,V6 = V44,V2 = V47,V49 >= 0,V42 >= 0,V43 >= 0,V7 = V49,V8 = V41]). eq(e3(V, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, Out),0,[],[Out = 0,V5 = V50,V51 >= 0,V52 >= 0,V9 = V53,V10 = V54,V55 >= 0,V56 >= 0,V50 >= 0,V1 = V56,V4 = V57,V58 >= 0,V59 >= 0,V = V51,V3 = V59,V57 >= 0,V6 = V55,V2 = V58,V60 >= 0,V53 >= 0,V54 >= 0,V7 = V60,V8 = V52]). eq(e1(V, V1, V2, V3, V4, Out),0,[],[Out = 0,V3 = V61,V62 >= 0,V63 >= 0,V2 = V64,V65 >= 0,V1 = V65,V4 = V63,V64 >= 0,V61 >= 0,V = V62]). input_output_vars(h1(Out),[],[Out]). input_output_vars(f2(Out),[],[Out]). input_output_vars(f1(Out),[],[Out]). input_output_vars(e4(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out),[V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10],[Out]). input_output_vars(e3(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out),[V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10],[Out]). input_output_vars(e2(V,V1,V2,V3,V4,Out),[V,V1,V2,V3,V4],[Out]). input_output_vars(e5(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(g2(Out),[],[Out]). input_output_vars(g1(Out),[],[Out]). input_output_vars(e1(V,V1,V2,V3,V4,Out),[V,V1,V2,V3,V4],[Out]). input_output_vars(h2(Out),[],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [e5/5]
1. non_recursive : [e1/6]
2. non_recursive : [e2/6]
3. non_recursive : [e4/12]
4. non_recursive : [e3/12]
5. non_recursive : [h1/1]
6. non_recursive : [h2/1]
7. non_recursive : [g1/1]
8. non_recursive : [g2/1]
9. non_recursive : [f1/1]
10. non_recursive : [f2/1]
11. non_recursive : [start/11]

#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is partially evaluated into e1/6
2. SCC is partially evaluated into e2/6
3. SCC is partially evaluated into e4/12
4. SCC is partially evaluated into e3/12
5. SCC is completely evaluated into other SCCs
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into g1/1
8. SCC is partially evaluated into g2/1
9. SCC is partially evaluated into f1/1
10. SCC is partially evaluated into f2/1
11. SCC is partially evaluated into start/11

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations e1/6
* CE 26 is refined into CE [27]
* CE 25 is refined into CE [28]


### Cost equations --> "Loop" of e1/6
* CEs [27] --> Loop 16
* CEs [28] --> Loop 17

### Ranking functions of CR e1(V,V1,V2,V3,V4,Out)

#### Partial ranking functions of CR e1(V,V1,V2,V3,V4,Out)


### Specialization of cost equations e2/6
* CE 22 is refined into CE [29]
* CE 21 is refined into CE [30]


### Cost equations --> "Loop" of e2/6
* CEs [29] --> Loop 18
* CEs [30] --> Loop 19

### Ranking functions of CR e2(V,V1,V2,V3,V4,Out)

#### Partial ranking functions of CR e2(V,V1,V2,V3,V4,Out)


### Specialization of cost equations e4/12
* CE 16 is refined into CE [31]
* CE 17 is refined into CE [32]
* CE 15 is refined into CE [33]


### Cost equations --> "Loop" of e4/12
* CEs [31] --> Loop 20
* CEs [32] --> Loop 21
* CEs [33] --> Loop 22

### Ranking functions of CR e4(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out)

#### Partial ranking functions of CR e4(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out)


### Specialization of cost equations e3/12
* CE 19 is refined into CE [34]
* CE 18 is refined into CE [35,36,37]
* CE 20 is refined into CE [38]


### Cost equations --> "Loop" of e3/12
* CEs [34,37] --> Loop 23
* CEs [36,38] --> Loop 24
* CEs [35] --> Loop 25

### Ranking functions of CR e3(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out)

#### Partial ranking functions of CR e3(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out)


### Specialization of cost equations g1/1
* CE 24 is refined into CE [39]


### Cost equations --> "Loop" of g1/1
* CEs [39] --> Loop 26

### Ranking functions of CR g1(Out)

#### Partial ranking functions of CR g1(Out)


### Specialization of cost equations g2/1
* CE 23 is refined into CE [40]


### Cost equations --> "Loop" of g2/1
* CEs [40] --> Loop 27

### Ranking functions of CR g2(Out)

#### Partial ranking functions of CR g2(Out)


### Specialization of cost equations f1/1
* CE 13 is refined into CE [41]
* CE 14 is refined into CE [42]


### Cost equations --> "Loop" of f1/1
* CEs [41,42] --> Loop 28

### Ranking functions of CR f1(Out)

#### Partial ranking functions of CR f1(Out)


### Specialization of cost equations f2/1
* CE 11 is refined into CE [43]
* CE 12 is refined into CE [44]


### Cost equations --> "Loop" of f2/1
* CEs [43,44] --> Loop 29

### Ranking functions of CR f2(Out)

#### Partial ranking functions of CR f2(Out)


### Specialization of cost equations start/11
* CE 2 is refined into CE [45]
* CE 3 is refined into CE [46]
* CE 4 is refined into CE [47]
* CE 5 is refined into CE [48,49,50]
* CE 6 is refined into CE [51,52,53]
* CE 7 is refined into CE [54,55]
* CE 8 is refined into CE [56]
* CE 9 is refined into CE [57]
* CE 10 is refined into CE [58,59]


### Cost equations --> "Loop" of start/11
* CEs [45,46,47,48,49,50,51,52,53,54,55,56,57,58,59] --> Loop 30

### Ranking functions of CR start(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10)

#### Partial ranking functions of CR start(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10)


Computing Bounds
=====================================

#### Cost of chains of e1(V,V1,V2,V3,V4,Out):
* Chain [17]: 2
with precondition: [V=0,V1=0,V2+V3+V4+1=Out,V2>=0,V3>=0,V4>=0]

* Chain [16]: 0
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0,V4>=0]


#### Cost of chains of e2(V,V1,V2,V3,V4,Out):
* Chain [19]: 1
with precondition: [V=0,V4=0,V1+V2+V3+1=Out,V1>=0,V2>=0,V3>=0]

* Chain [18]: 1
with precondition: [V=V1,V3=V4,V+V2+V3+1=Out,V>=0,V2>=0,V3>=0]


#### Cost of chains of e4(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out):
* Chain [22]: 2
with precondition: [V=0,V1=0,V2=0,V3=0,V4=0,V5=0,V6=0,V7=0,V8+V9+V10+1=Out,V8>=0,V9>=0,V10>=0]

* Chain [21]: 0
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0,V6>=0,V7>=0,V8>=0,V9>=0,V10>=0]

* Chain [20]: 1
with precondition: [V=V1,V=V2,V=V3,V=V4,V=V5,V=V6,V=V7,V=V8,V=V9,V=V10,3*V+1=Out,V>=0]


#### Cost of chains of e3(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10,Out):
* Chain [25]: 3
with precondition: [V=0,V1=0,V2=0,V3=0,V4=0,V5=0,V6=0,V7=0,V8+V9+V10+1=Out,V8>=0,V9>=0,V10>=0]

* Chain [24]: 1
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0,V6>=0,V7>=0,V8>=0,V9>=0,V10>=0]

* Chain [23]: 2
with precondition: [V=V2,V1=V3,V1=V4,V1=V6,V5=V7,V=V8,V1=V9,V5=V10,V+V1+V5+1=Out,V>=0,V1>=0,V5>=0]


#### Cost of chains of g1(Out):
* Chain [26]: 2
with precondition: [Out=0]


#### Cost of chains of g2(Out):
* Chain [27]: 2
with precondition: [Out=0]


#### Cost of chains of f1(Out):
* Chain [28]: 3
with precondition: [Out=0]


#### Cost of chains of f2(Out):
* Chain [29]: 3
with precondition: [Out=0]


#### Cost of chains of start(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10):
* Chain [30]: 3
with precondition: []


Closed-form bounds of start(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10):
-------------------------------------
* Chain [30] with precondition: []
- Upper bound: 3
- Complexity: constant

### Maximum cost of start(V,V1,V2,V3,V4,V5,V6,V7,V8,V9,V10): 3
Asymptotic class: constant
* Total analysis performed in 365 ms.

(12) BOUNDS(1, 1)